(set-option :smt.arith.propagate_eqs false)
(set-option :rewriter.flat false)
(set-option :smt.phase_selection 5)
(set-option :smt.threads 4)
(set-option :smt.string_solver z3str3)
(declare-const Str0 String)
(declare-const Str5 String)
(declare-const Str7 String)
(declare-const Str10 String)
(declare-const Str12 String)
(declare-const Str13 String)
(declare-const Str16 String)
(declare-const Str17 String)
(declare-const Str18 String)
(declare-const v16 Bool)
(assert-soft (or (distinct Str5 Str17 Str0 (str.++ Str5 Str7 Str16 Str12) (str.++ Str18 Str13 Str10 "viqwxc" Str5)) v16))
(assert-soft (or (distinct Str5 Str17 Str0 (str.++ Str5 Str7 Str16 Str12) (str.++ Str18 Str13 Str10 "viqwxc" Str5))))
(check-sat)